nLab homotopy type theory FAQ

under construction

This page is to provide non-technical or maybe semi-technical discussion of the nature and role of the foundational system for mathematics known as homotopy type theory. For more technical details and further pointers see at homotopy type theory.

FAQ

What is homotopy type theory?

For the person on the street

Homotopy type theory is a theory of objects, which we call terms, collections of objects, which we call types, and equalities between any two objects in a collection, which we call identity types.

One fundamental aspect of mathematics is that equalities between different collections of objects behave differently from each other. If we have a type where for all terms have exactly one identity between them, this is called a proposition or a truth value. The type with no terms is trivially a proposition, as every single one of the nonexistent terms have exactly one identity between them.

However, not all types are propositions: take the type with two distinct terms $a$ and $b$, there is no identity between $a$ and $b$. The identity types between two terms here are propositions, and the types are called sets.

Still, not all types are sets: take the type of sets with two terms, the first one with terms $a$ and $b$, and the second one with terms $c$ and $d$. There are two ways to say that these types are equal: by adding an identity between $a$ and $c$ and between $b$ and $d$, or by adding an identity between $a$ and $d$ and between $b$ and $c$. Thus, the identity types between the two sets is set-valued, rather than proposition-valued, and the type is a groupoid, rather than a set. In this way, we could say that, for example, the set of positive integers is equal to the set of negative integers, or that the set of complex numbers is equal to the set of ordered pairs of real numbers.

One could continue the process, yielding 2-groupoids whose identity types are groupoids, 3-groupoids whose identity types are 2-groupoids, and so forth. And finally, one could have types whose identity types are general types: these types are also known as $\infty$-groupoids.

For set theorists

Homotopy type theory is a refinement of constructive set theory that takes fully seriously the constructive nature also of identity. (As with all constructive mathematics, with the relevant axioms added, this subsumes, rather than excludes, classical mathematics, see below at Is HoTT limited to constructive mathematics?.)

It is this insistence on constructive witnesses for identity and on witnesses for identity of such witnesses, and so ever on, that makes what in traditional set theory are just sets (whose elements are either equal or not) in homotopy type theory instead be groupoids (whose elements may have non-trivial isomorphism between them) and indeed 2-groupoids (with isomorphisms between these isomorphisms) and so ever on; hence what makes what used to be just sets be what is kown as ∞-groupoids or homotopy types.

More technically, restriction to the 0-truncated types in HoTT (the “h-sets”) gives a predicative topos “of sets”, and a topos if one allows the resizing axiom (details are here). When adding the axiom of choice to HoTT, one obtains a model of ETCS. The iterative notion of set can also be captured. Aczel’s sets-as-trees interpretation gives a model of constructive set theory CZF. Again by adding choice to HoTT, one obtains a model of ZFC; see Ch10 of the HoTT book.

Conversely HoTT has models in ZFC (+a number of Grothendieck universes to model the type theoretic universes), namely in structures called (∞,1)-toposes which are presented by presheaves of simplicial sets. (See also at Does HoTT have models in infinity-toposes?)

The nature and role of these higher toposes in HoTT may be understood by analogy with the familar forcing models: When one proves something in ZF, it is automatically also true in all forcing extensions. The same is true for constructive set theory, except that there are more forcing extensions since we don’t have to force the law of excluded middle; those constructive notions of forcing (which also subsume permutation models) are called “sites” and their models are called “1-toposes”. Now in HoTT we have an even more general sort of forcing appropriate for homotopy theory, called (∞,1)-sites, whose models are called (∞,1)-toposes.

For type theorists

(…)

For homotopy theorists

(…)

Why should I care?

For the person on the street

Homotopy type theory is a foundation upon which all of mathematics is based upon. Every collection of objects in mathematics, such as the collection of natural numbers, collection of real numbers, collection of strings of characters in an alphabet, collection of propositions and the collection of all sets, is represented in homotopy type theory. It is also a language in which one could do mathematics in, from algebra to geometry to calculus.

For set theorists

Traditional set theory is formulated in first-order logic. Under the propositions as types interpretation, first order logic maps soundly and completely into type theory (Martin-Löf 74, section 3.1, Barendregt 91, section 4). But now the homotopy 0-types in homotopy type theory already give a constructive set theory, natively, without further axiomatization. See at h-set for more.

For type theorists

For homotopy theorists

Most homotopy-theoretic theorems that are proven in the HoTT textbook are, in their traditional informal version, material of a first-year course on homotopy theory. Experts who do not care about formal proof might not be impressed yet.

But the point is that there is significant prospect. By the discussion at Does HoTT have models in infinity-toposes, it is a fact that homotopy type theory is the internal language of (∞,1)-toposes, hence of the most powerful modern incarnation of homotopy theory. Whether or not anyone has already made impressive use of this fact (but see below), this is of genuine interest in homotopy theory irrespective of the issue of formal proof.

Historically, making use of the internal logic-perspective of elementary toposes led to substantial insight into all theory that uses Grothendieck toposes, such as notably algebraic geometry. While Lurie‘s book Higher Topos Theory based on Charles Rezk’s note Homotopy Topos Theory is an astounding piece of work, it falls short of saying anything about this crucial internal aspect of (higher) topos theory. Homotopy type theory is precisely what fills this gap. For more on how this works see at HoTT methods for homotopy theorists.

An illustration of the use of this is the proof of the Blakers-Massey theorem. This basic fact of homotopy theory has a classical proof in the classical homotopy category ∞Grpd $\simeq$ $L_{whe}$ Top, a proof that is however rather roundabout. From this follows a proof in all (∞,1)-toposes with an (∞,1)-site of definition by, essentially, reducing stalkwise to the classical theorem (details are here). But now the theorem was also proven in homotopy type theory (details are here). Translating this formal proof back to ordinary language produces first of all a new and more elegant proof of Blakers-Massey in ∞Grpd $\simeq$ $L_{whe}$ Top, second a new and elegant proof of the statement for (∞,1)-toposes with (∞,1)-site of definition. This is something that some homotopy theorists tried to find by classical means and failed (details are here). And moreover, the HoTT proof of Blakers-Massey is actually a new result when applied to elementary (∞,1)-toposes, where the classical methods of proving it completely break down.

It seems rather plausible that this is just a simple first example of a future where HoTT methods allow to enter new territory in classical homotopy theory. Of course it will require some expert homotopy theorists to seriously look into the internal-language-of-$\infty$-toposes way of doing homotopy theory. This is now an open problem for homotopy theorists just as it is for type theorists.

What role does the univalence axiom play?

For the person on the street

The axiom of univalence may be thought of as a formalization of what might be called the principle of equivalence of mathematics, which is the basic but important idea that mathematical structures which are equivalent should behave the same, satisfy the same theorems and so forth.

In particular, in elementary Euclidean geometry, two shapes are traditionally said to be equal or congruent to each other if there is an isometry (distance-preserving transformation) between the two shapes. Usually, this congruence requires the need for a quotient of the isomorphism classes in the category of geometric shapes, but with univalence, one does not need such a construction: equality of shapes is the isometries between the shapes.

Obvious as this may seem, this principle may be violated in other foundations of mathematics such as ZFC. On the other hand, while these models allow such violation, in practice one essentially never wants to use such violation. The univalence axiom hence serves to make formal mathematical foundation be closer to the actual “nature of mathematics”, at least to the practice of mathematics.

For set theorists

For type theorists

The axiom of univalence added to Martin-Löf type theory implies all of the following:

1. functional extensionality

2. quotient types

3. higher inductive types with nontrivial homotopies,

   Which in turn imply a wealth of further structure such as (but not limited to)

   1. bracket types

   2. etc.

For homotopy theorists

In view of the answer at Does HoTT have interpretation in infinity-toposes? the axiom of univalence axiomatizes the presence of an object classifier in an (∞,1)-topos $\mathbf{H}$ (details are here).

In the default choice $\mathbf{H} =$∞Grpd $\simeq$ $L_{whe}$Top of traditonal homotopy theory this is the universal fibration over the disjoint union of classifying spaces $\coprod_{[F]} B Aut(F)$ of the automorphism ∞-groups of all (small) homotopy types $[F]$.

Therefore from the axiom of univalence follows for instance the theory of ∞-actions, associated ∞-bundles and of twisted cohomology (details are here).

What advantages does homotopy type theory have over set theory?

As explained at What is HoTT for set theorists?, HoTT subsumes set theory. It has all the advantages that structural set theory (Algebraic set theory, ETCS) has over material set theory (ZFC), but moreover it allows us to natively capture higher categorical (more precisely, higher groupoidal) and homotopical reasoning. Moreover, as a practical foundation, set theory may be compared to the Turing machine model, or perhaps more generously, say, ALGOL. Whereas, homotopy type theory is closely related to modern programming languages like Haskell and ML, or more accurately Coq and Agda.

Is homotopy type theory limited to constructive mathematics?

No. On the 0-types (the h-sets) the axioms of classical logic may be imposed, such as the law of excluded middle (details are here) and the axiom of choice (details are here).

One model that interprets the resulting axioms is the standard model in simplicial sets (here) inside ZFC+inaccessible cardinals. The 0-types in this model are precisely the ordinary sets in ZFC. See also the discussion at What is HoTT? For set theorists.

For more exposition see also

• Andrej Bauer, Univalent foundations subsume classical mathematics (2013)

Does HoTT have interpretation/semantics/models in $\infty$-toposes?

The short answer is: Yes. Homotopy type theory has higher categorical semantics in every (∞,1)-topos, in refinement of how plain dependent type theory has categorical semantics in toposes.

The more detailed answer depends on which axiomatics precisely one subsumes under “homotopy type theory”. A hierarchy of three main variants (“fragments”) of homotopy type theory should be distinguished here:

1. HoTT without univalent type universes;

2. HoTT with univalent weak type universes à la Tarski;

3. HoTT with univalent strict type universes à la Russell or à la Tarski;

In all three cases the $\infty$-categorical semantics is induced by ordinary categorical semantics in a type-theoretic model category which in turn presents an (∞,1)-category. The way this works is reviewed also at HoTT methods for homotopy theorists. This relies on standard techniques for interpreting any dependent type theory in a locally cartesian closed category (see here for details).

With that understood, the higher categorical semantics for the above three cases is as follows:

1. HoTT without univalent universes has semantics in every locally presentable locally cartesian closed (∞,1)-category (details are here).

2. HoTT with strict univalent universes has semantics at least in (∞,1)-presheaf (∞,1)-toposes over elegant Reedy categories. This includes in particular the standard base (∞,1)-topos ∞Grpd as well as for instance the Sierpinski (∞,1)-topos (details are here).

3. HoTT with weak univalent universes has semantics in every (∞,1)-sheaf (∞,1)-topos (details are here).

Since we are assuming local presentability here, all these models have enough (∞,1)-colimits to interpret higher inductive types. (One might also ask for models of HoTT without univalence and without higher inductive types and would expect that this then also includes locally cartesian closed (∞,1)-categories which are not necessarily locally presentable.)

One may also ask about models in elementary (∞,1)-toposes. Their theory or even definition is however much in the making. On the other hand, existing proposals essentially turn the question around and define elementary (∞,1)-toposes as (∞,1)-categories with the minimum of properties such that HoTT may be modeled in them. This reflects the idea that what is “elementary” about elementary $(\infty,1)$-toposes is precisely the fact that there is an internal type theory language for them.

In conclusion, every proposition proven in homtopy type theory yields (subject to the above qualification) a statement that holds true in every (∞,1)-topos (in every presentable locally cartesian closed (∞,1)-category), i.e. homotopy type theory is the internal language of $\infty$-toposes.

If one wishes to prove statements that hold only in some class of $\infty$-toposes, then one needs to add further axioms to HoTT that characterize these classes. For instance adding higher modalities that define cohesive homotopy type theory make it a language that proves theorems which hold in all cohesive (∞,1)-toposes.

What is meant by a “computational interpretation of univalence”?

Some type theorists care about canonicity, which is essentially having terms of types be judgmentally equal to canonical forms. For example, the canonical form of terms in the natural numbers is either $0$ or $s(n)$ where $n$ is a canonical form of the natural numbers, and the canonical form of terms in identity types is reflexivity. Canonicity is an important computational trait for dependent type theories to have as it makes implementing the type theory in a proof assistant easier.

However, the univalence axiom in Martin-Löf type theory causes some terms of identity types to not be judgmentally equal to the canonical form of reflexivity, which breaks canonicity. As a result, some type theorists have looked for alternative dependent type theories which have both canonicity and univalence, such as cubical type theory and higher observational type theory, the latter of which is still a work in progress as of 2024.

Alternatively, Vladimir Voevodsky proposed a variant of canonicity called homotopy canonicity which replaces the judgmental equality of terms to canonical forms with identifications of terms with canonical forms: there is an identification between every term of a type and a canonical form, and there is an effective algorithm to compute such identifications (see Sattler 2019). In this sense, the univalence axiom is computationally valid since it satisfies homotopy canonicity.

More generally, many axioms which break canonicity still satisfy homotopy canonicity, such as function extensionality, UIP and typal axiom K, propositional extensionality, descent, and univalence. However, excluded middle and the axiom of choice still break homotopy canonicity, so any computational interpretation of dependent type theory based on homotopy canonicity remains constructive.

What are higher inductive types?

What do we gain by a proof in homotopy type theory of $\pi_1(S^1) = \mathbb{Z}$ over ordinary proofs?

Is it possible to define higher coinductive types?

Yes, it is currently possible to define higher coinductive types as homotopy-terminal coalgebras for an endofunctor. Homotopy-terminal coalgebras for an endofunctor are like the usual notion of terminal coalgebra for an endofunctior, but where equality is expressed via the identity type instead of judgmental equality and uniqueness is expressed via contractibility in the definition. However, the resulting higher coinductive types will only have typal beta-conversion and eta-conversion rules, since only the typal versions are derivable from the universal property of homotopy-terminal coalgebras for an endofunctor as expressed in dependent type theory.

In what sense does homotopy type theory already contain logic?

A proposition can be defined as a type such that the identity type between any two terms of the type has a term. One could add to homotopy type theory the higher inductive type of propositional truncation, which takes any type and turns it into a proposition. The propositional truncation of product types correspond to conjunction, the propositional truncation of sum types correspond to disjunction, the propositional truncation of function types correspond to implication, the propositional truncation of dependent product types correspond to universal quantification, the propositional truncation of dependent sum types correspond to existential quantification, the empty type corresponds to false, a function type into the empty type corresponds to negation, and contractible types correspond to true. This corresponds to constructive predicate logic, and the addition of the axiom of excluded middle to the type theory yields classical predicate logic.

Can category theory be carried out in homotopy type theory?

Yes. One could define a category as a type $C$ whose identity types $a =_C b$ for $a:C$ and $b:C$ are sets, with a set $M$ with functions $s:M \to C$, $t:M \to C$, $id:C \to M$ and function

$$c:\left(\sum_{f:M} \sum_{g:M} t(f) =_C s(g)\right) \to M$$

such that $s(c(g,f)) =_C s(f)$ and $t(c(g,f)) =_C t(g)$, for every $f:M$, $c(f, id(s(f))) =_M f$ and $c(id(t(f)), f) =_M f$, and for every $f:M$, $g:M$, and $h:M$ such that $t(f) =_C s(g)$ and $t(g) =_C s(h)$, $c(h,c(g,f)) =_M c(c(h,g),f)$.

Then one could define a functor between categories $(C,M)$ and $(D,N)$ as a function $F:C \to D$ with a function $G:M \to N$ such that for all $f:M$, $F(s_C(f)) =_D s_D(G(f))$ and $F(t_C(f)) =_D t_D(G(f))$, for all $a:C$, $G(id_C(a)) =_N id_D(F(a))$, and for terms $f:M$ and $g:M$ such that $t(f) =_D s(g)$, $G(g \circ_C f) =_N F(g) \circ_D F(h)$.

Can $(\infty,1)$-categories be defined in homotopy type theory?

It is currently unknown how to define the coherence theorems necessary to define $(\infty,1)$-categories in vanilla homotopy type theory. There are other approaches to type theory such as directed homotopy type theory which might be able to define $(\infty,1)$-categories.

Related articles

• homotopy theory FAQ